Why do they have to be the same level? why not generalize it more so that they can all be different levels

The original proof does not type check if I just simply assigning the types with different levels. I renamed it into join-assoc-samelevel and wrote a new join-assoc using the old one that supports different levels.

The original proof does not type check if I just simply assigning the types with different levels.

Why would that be? only reason I can think of is that the lemmas it was using (spanEquivToPushoutPath and 3x3-span.3x3-lemma) weren't level-polymorphic enough, but if thats the case why not generalize them too?

Ah, I think I see the problem. All the lemmas you're using are fully polymorphic, but I think the only problem is that it uses paths instead of equivalences. So you could make another lemma called join-assoc-≃ and use the equivalence version of all the lemmas (use isoToEquiv 3x3-Iso instead of 3x3-lemma, and apply pathToEquiv to spanEquivToPushoutPath). Afterwards you could then turn it into join-assoc using univalence. This would definitely be better than messing with Lifts, and it would be more useful to have an equivalence version as well<\del>

Oh wait, joinAssocDirect already exists